A:Type, eq:EqDecider(A), B:(AType), g:x:A fp B(x), x:A.
(x  dom(g))  (fpf-normalize(eq;g)(x) = g(x)  B(x)) 

latex

Definitions

f(x), x  dom(f), f(x)?z, , f  g, x : v, fpf-normalize(eq;g), x:A  B(x), a:A fp B(a), Type, t  T, x:A. B(x), EqDecider(T), x:AB(x), f(a), x(s), x. t(x), x.A(x), Top, b, P  Q, , ff, eqof(d), p q, if b then t else f fi , reduce(f;k;as), [], <a, b>, t.2, t.1, b, filter(P;l), [car / cdr], s ~ t, Void, x:A.B(x), s = t, (x  l), {x:A| B(x)} , type List, False, deq-member(eq;x;L), , A, , P & Q, P  Q, Unit, left + right, S  T, P  Q, {T}, P  Q

Lemmas

cons member, subtype rel self, implies functionality wrt iff, assert-deq-member, deq property, deq-member wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, eqof wf, bool wf, false wf, list-subtype, l member wf, top wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf wf, deq wf